Termination of the following Term Rewriting System could be disproven:
Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:
U12(tt) → snd(splitAt(N, XS))
U161(tt) → cons(N)
U172(tt) → head(afterNth(N, XS))
U182(tt) → Y
U191(tt) → pair(nil, XS)
U203(tt) → U204(splitAt(N, XS))
U204(pair(YS, ZS)) → pair(cons(X), ZS)
U212(tt) → XS
U22(tt) → X
U222(tt) → fst(splitAt(N, XS))
U32(tt) → N
U101(tt) → U102(isLNat)
U102(tt) → tt
U11(tt) → U12(isLNat)
U111(tt) → tt
U121(tt) → tt
U131(tt) → U132(isLNat)
U132(tt) → tt
U141(tt) → U142(isLNat)
U142(tt) → tt
U151(tt) → U152(isLNat)
U152(tt) → tt
U171(tt) → U172(isLNat)
U181(tt) → U182(isLNat)
U201(tt) → U202(isNatural)
U202(tt) → U203(isLNat)
U21(tt) → U22(isLNat)
U211(tt) → U212(isLNat)
U221(tt) → U222(isLNat)
U31(tt) → U32(isLNat)
U41(tt) → U42(isLNat)
U42(tt) → tt
U51(tt) → U52(isLNat)
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural)
fst(pair(X, Y)) → U21(isLNat)
head(cons(N)) → U31(isNatural)
isLNat → tt
isLNat → U41(isNatural)
isLNat → U51(isNatural)
isLNat → U61(isPLNat)
isLNat → U71(isNatural)
isLNat → U81(isPLNat)
isLNat → U91(isLNat)
isLNat → U101(isNatural)
isNatural → tt
isNatural → U111(isLNat)
isNatural → U121(isNatural)
isNatural → U131(isNatural)
isPLNat → U141(isLNat)
isPLNat → U151(isNatural)
natsFrom(N) → U161(isNatural)
sel(N, XS) → U171(isNatural)
snd(pair(X, Y)) → U181(isLNat)
splitAt(0, XS) → U191(isLNat)
splitAt(s(N), cons(X)) → U201(isNatural)
tail(cons(N)) → U211(isNatural)
take(N, XS) → U221(isNatural)
↳ GTRS
↳ CritRuleProof
Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:
U12(tt) → snd(splitAt(N, XS))
U161(tt) → cons(N)
U172(tt) → head(afterNth(N, XS))
U182(tt) → Y
U191(tt) → pair(nil, XS)
U203(tt) → U204(splitAt(N, XS))
U204(pair(YS, ZS)) → pair(cons(X), ZS)
U212(tt) → XS
U22(tt) → X
U222(tt) → fst(splitAt(N, XS))
U32(tt) → N
U101(tt) → U102(isLNat)
U102(tt) → tt
U11(tt) → U12(isLNat)
U111(tt) → tt
U121(tt) → tt
U131(tt) → U132(isLNat)
U132(tt) → tt
U141(tt) → U142(isLNat)
U142(tt) → tt
U151(tt) → U152(isLNat)
U152(tt) → tt
U171(tt) → U172(isLNat)
U181(tt) → U182(isLNat)
U201(tt) → U202(isNatural)
U202(tt) → U203(isLNat)
U21(tt) → U22(isLNat)
U211(tt) → U212(isLNat)
U221(tt) → U222(isLNat)
U31(tt) → U32(isLNat)
U41(tt) → U42(isLNat)
U42(tt) → tt
U51(tt) → U52(isLNat)
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
afterNth(N, XS) → U11(isNatural)
fst(pair(X, Y)) → U21(isLNat)
head(cons(N)) → U31(isNatural)
isLNat → tt
isLNat → U41(isNatural)
isLNat → U51(isNatural)
isLNat → U61(isPLNat)
isLNat → U71(isNatural)
isLNat → U81(isPLNat)
isLNat → U91(isLNat)
isLNat → U101(isNatural)
isNatural → tt
isNatural → U111(isLNat)
isNatural → U121(isNatural)
isNatural → U131(isNatural)
isPLNat → U141(isLNat)
isPLNat → U151(isNatural)
natsFrom(N) → U161(isNatural)
sel(N, XS) → U171(isNatural)
snd(pair(X, Y)) → U181(isLNat)
splitAt(0, XS) → U191(isLNat)
splitAt(s(N), cons(X)) → U201(isNatural)
tail(cons(N)) → U211(isNatural)
take(N, XS) → U221(isNatural)
The rule U12(tt) → snd(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.